g:IMonoid, b:. (when b. e) = e  |g| 

latex

Up	groups 1
Definitions of Statement	IMonoid, when b. p
Definitions	ff, tt, t  T, if b then t else f fi , when b. p, x:A. B(x), Unit, , IMonoid,
Lemmas	imon wf, bool wf, grp id wf